(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_IDL)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(assert (let ((e2 0))
(let ((e3 4))
(let ((e4 1))
(let ((e5 (>= (- v0 v1) (- e4))))
(let ((e6 (= v0 v0)))
(let ((e7 (<= (- v1 v0) (- e3))))
(let ((e8 (<= (- v1 v0) (- e2))))
(let ((e9 (distinct (- v1 v1) (- e3))))
(let ((e10 (> v0 v0)))
(let ((e11 (> (- v0 v1) e2)))
(let ((e12 (> (- v0 v1) (- e3))))
(let ((e13 (> (- v1 v0) (- e2))))
(let ((e14 (= v0 v0)))
(let ((e15 (distinct (- v0 v0) e2)))
(let ((e16 (>= (- v1 v1) e2)))
(let ((e17 (<= (- v1 v1) (- e3))))
(let ((e18 (distinct (- v0 v0) (- e3))))
(let ((e19 (distinct (- v0 v1) e4)))
(let ((e20 (> v0 v1)))
(let ((e21 (> (- v1 v0) (- e3))))
(let ((e22 (> v0 v0)))
(let ((e23 (= (- v0 v1) (- e2))))
(let ((e24 (> (- v0 v1) e2)))
(let ((e25 (> (- v0 v0) e3)))
(let ((e26 (> v1 v1)))
(let ((e27 (= (- v0 v1) e2)))
(let ((e28 (= (- v1 v0) e4)))
(let ((e29 (< v0 v1)))
(let ((e30 (>= (- v0 v1) (- e3))))
(let ((e31 (< (- v0 v0) (- e4))))
(let ((e32 (and e31 e13)))
(let ((e33 (=> e18 e29)))
(let ((e34 (or e23 e33)))
(let ((e35 (ite e5 e24 e7)))
(let ((e36 (or e20 e26)))
(let ((e37 (xor e9 e22)))
(let ((e38 (ite e28 e19 e21)))
(let ((e39 (ite e38 e14 e25)))
(let ((e40 (ite e36 e16 e15)))
(let ((e41 (or e12 e34)))
(let ((e42 (= e30 e41)))
(let ((e43 (not e40)))
(let ((e44 (xor e17 e32)))
(let ((e45 (or e6 e8)))
(let ((e46 (not e35)))
(let ((e47 (= e42 e27)))
(let ((e48 (xor e10 e45)))
(let ((e49 (= e11 e46)))
(let ((e50 (not e49)))
(let ((e51 (=> e43 e50)))
(let ((e52 (xor e47 e44)))
(let ((e53 (xor e48 e37)))
(let ((e54 (xor e52 e53)))
(let ((e55 (not e39)))
(let ((e56 (= e54 e54)))
(let ((e57 (and e51 e51)))
(let ((e58 (or e57 e57)))
(let ((e59 (= e55 e55)))
(let ((e60 (= e56 e56)))
(let ((e61 (= e58 e60)))
(let ((e62 (not e61)))
(let ((e63 (= e62 e59)))
e63
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)
